\begin{tabbing}
$\forall$${\it the\_es}$:event\_system\{i:l\}, $e$:es{-}E(${\it the\_es}$).
\\[0ex]($\uparrow$es{-}isrcv(${\it the\_es}$; $e$))
\\[0ex]$\Rightarrow$ (\=es{-}index(${\it the\_es}$; $e$)\+
\\[0ex]$\in$ int\_seg(0; $\parallel$es{-}sends(${\it the\_es}$; es{-}lnk(${\it the\_es}$; $e$); es{-}sender(${\it the\_es}$; $e$))$\parallel$))
\-
\end{tabbing}